/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓John McCarthy

␈↓ α∧␈↓␈↓ αTMy␈α
discussion␈α
will␈αfocus␈α
on␈α
two␈α
topics:␈αthe␈α
present␈α
status␈α
of␈αthe␈α
problems␈α
discussed␈α
in␈αmy
␈↓ α∧␈↓"Problems␈α
in␈αthe␈α
Theory␈αof␈α
Computation"␈αgiven␈α
at␈αthe␈α
1965␈αWorld␈α
Computer␈αCongress␈α
in␈αNew
␈↓ α∧␈↓York.␈α∂ The␈α∂second␈α∂topic␈α∂concerns␈α∂features␈α∂of␈α∂natural␈α∂language␈α∂description␈α∂of␈α∂processes␈α∂not␈α∂yet
␈↓ α∧␈↓offered in programming languages.

␈↓ α∧␈↓␈↓ αTMy 1965 paper begins

␈↓ α∧␈↓␈↓ αT␈↓↓"The␈αprize␈αto␈αbe␈α
won␈αif␈αwe␈αcan␈α
develop␈αa␈αreasonable␈αmathematical␈α
theory␈αof␈αcomputation␈αis␈α
the
␈↓ α∧␈↓↓elimination␈α∞of␈α
debugging.␈α∞ Instead,␈α
a␈α∞programmer␈α∞will␈α
prepare␈α∞a␈α
computer-checked␈α∞proof␈α∞that␈α
a
␈↓ α∧␈↓↓program has the desired properties.

␈↓ α∧␈↓. . .

␈↓ α∧␈↓␈↓ αT␈↓↓I␈αbelieve␈αthat␈αthis␈αgoal␈αcan␈αbe␈αachieved,␈αbut␈αwe␈αare␈αa␈αlong␈αway␈αfrom␈αit␈αnow.␈α The␈αpurpose␈αof
␈↓ α∧␈↓↓this␈α
paper␈αis␈α
to␈αlist␈α
some␈αsubgoals.␈α
 In␈αmy␈α
opinion␈αeach␈α
of␈αthese␈α
problems␈αis␈α
solvable,␈αis␈α
theoretically
␈↓ α∧␈↓↓interesting, and contributes to the understanding required for a practical theory"␈↓.

␈↓ α∧␈↓␈↓ αTIn␈α∪1965␈α∪the␈α∪only␈α∪approach␈α∪to␈α∪proving␈α∪programs␈α∪correct␈α∪was␈α∪the␈α∪functional␈α∩approach
␈↓ α∧␈↓described␈α
in␈α∞my␈α
two␈α
1963␈α∞papers.␈α
 Floyd's␈α∞inductive␈α
assertion␈α
method,␈α∞anticipated␈α
by␈α∞Turing␈α
in
␈↓ α∧␈↓connection␈αwith␈αa␈αparticular␈αprogram␈αin␈α1945,␈αwas␈αnot␈αpublished␈αtill␈α1967.␈α Since␈αthat␈αtime␈αthere
␈↓ α∧␈↓has␈αbeen␈αan␈αexplosion␈αof␈αeffort␈αin␈αdeveloping␈αprogram␈αverification␈αmethods,␈αbut␈αthe␈αabove␈αgoals
␈↓ α∧␈↓are still in the future.

␈↓ α∧␈↓␈↓ αTHere is a summary of the problems listed in that paper.

␈↓ α∧␈↓␈↓ αT1.␈α∞Develop␈α∞a␈α∞language␈α∂for␈α∞expressing␈α∞facts␈α∞about␈α∞programs␈α∂that␈α∞accepts␈α∞proofs␈α∞close␈α∂to␈α∞a
␈↓ α∧␈↓programmer's informal reasoning.  There is some progress.

␈↓ α∧␈↓␈↓ αT2. Express properties of programs not known to terminate.  This is now well understood.

␈↓ α∧␈↓␈↓ αT3.␈α
Conventions␈α∞for␈α
describing␈α
languages,␈α∞data␈α
spaces,␈α
computers␈α∞and␈α
algorithms␈α
in␈α∞such␈α
a
␈↓ α∧␈↓form that the relations among them can be explored.  There still isn't a satisfactory general system.

␈↓ α∧␈↓␈↓ αTHere were some specific problems.

␈↓ α∧␈↓␈↓ αT1.␈αExtend␈αfirst␈αorder␈αlogic␈αto␈αinclude␈αpartial␈αpredicates␈αand␈αfunctions.␈α This␈αhas␈αbeen␈αdone
␈↓ α∧␈↓in␈α∪various␈α∪ways.␈α∩ Notable␈α∪are␈α∪(Scott,␈α∩many␈α∪papers),␈α∪(Cartwright␈α∩1976)␈α∪and␈α∪(Cartwright␈α∩and
␈↓ α∧␈↓McCarthy 1979).

␈↓ α∧␈↓␈↓ αT2.␈α∞Develop␈α∂the␈α∞state␈α∂vector␈α∞approach␈α∞to␈α∂the␈α∞semantics␈α∂of␈α∞programming␈α∂languages.␈α∞ Much
␈↓ α∧␈↓has been done in this direction.

␈↓ α∧␈↓␈↓ αT3.␈α∞Develop␈α
a␈α∞theory␈α∞of␈α
syntax␈α∞directed␈α
computing.␈α∞ Almost␈α∞nothing␈α
has␈α∞been␈α∞done␈α
except
␈↓ α∧␈↓for informal proofs about specific syntax directed algorithms.
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓New Problems:

␈↓ α∧␈↓␈↓ αTMy␈α
1965␈α
paper␈αwas␈α
directed␈α
to␈α
a␈αparticular␈α
area␈α
of␈α
computer␈αscience,␈α
and␈α
the␈α
present␈αtask␈α
is
␈↓ α∧␈↓more general.  Here are some goals.

␈↓ α∧␈↓␈↓ αT1.␈α⊃An␈α∩approximate␈α⊃quantitative␈α∩theory␈α⊃allowing␈α∩one␈α⊃to␈α∩divide␈α⊃the␈α∩size␈α⊃of␈α∩the␈α⊃abstract
␈↓ α∧␈↓execution␈α∞of␈α∂an␈α∞algorithm␈α∂by␈α∞the␈α∂speed␈α∞of␈α∞a␈α∂computer␈α∞to␈α∂get␈α∞the␈α∂time␈α∞required.␈α∂ Consider,␈α∞for
␈↓ α∧␈↓example,␈α∂suppose␈α∞one␈α∂wanted␈α∞to␈α∂have␈α∞a␈α∂computer␈α∞chess␈α∂tournament␈α∞where␈α∂the␈α∂computers␈α∞were
␈↓ α∧␈↓handicapped␈α∞according␈α∂to␈α∞speed,␈α∂so␈α∞that␈α∞algorithms␈α∂rather␈α∞than␈α∂whole␈α∞systems␈α∂were␈α∞competing.
␈↓ α∧␈↓This is an old question, but it needs to be revived from time to time.

␈↓ α∧␈↓␈↓ αT2.␈α∪Programming␈α∪languages␈α∩that␈α∪allow␈α∪more␈α∩of␈α∪the␈α∪essential␈α∩useful␈α∪features␈α∪of␈α∩natural
␈↓ α∧␈↓language.␈α∪ In␈α∪my␈α∀view␈α∪the␈α∪syntax␈α∪of␈α∀natural␈α∪language␈α∪is␈α∪not␈α∀its␈α∪main␈α∪useful␈α∀feature,␈α∪and
␈↓ α∧␈↓experience␈αhas␈αshown␈αthat␈αprogramming␈αlanguages␈αthat␈αmerely␈αrequire␈αEnglish␈αsyntax␈αbe␈αused␈αto
␈↓ α∧␈↓express␈α
the␈α
same␈α
programs␈α
that␈α
could␈α
be␈α∞written␈α
in␈α
Algol␈α
is␈α
not␈α
an␈α
advance.␈α∞ COBOL's␈α
utility,
␈↓ α∧␈↓such as it is, is based on its semantic features and not on its syntax.

␈↓ α∧␈↓␈↓ αTa.␈αA␈αkey␈αfeature␈αof␈αnatural␈αlanguage␈αis␈αthe␈αability␈αto␈αrequest␈αa␈αmodified␈αprocedure␈αwithout
␈↓ α∧␈↓fully␈α∀understanding␈α∃the␈α∀original␈α∀procedure.␈α∃ For␈α∀example,␈α∀an␈α∃airline␈α∀official␈α∀could␈α∃tell␈α∀his
␈↓ α∧␈↓programmers␈αto␈αhave␈αthe␈αreservation␈αprogram␈αask␈αfor␈αthe␈αnationality␈αof␈αthe␈αpassenger␈αand␈αavoid
␈↓ α∧␈↓seating␈α
nationals␈α
of␈αspecified␈α
warring␈α
countries␈α
next␈αto␈α
each␈α
other.␈α
 In␈αorder␈α
to␈α
do␈α
this,␈αthe␈α
official
␈↓ α∧␈↓doesn't␈αhave␈αto␈αknow␈αhow␈αthe␈αexisting␈αprogram␈αworks.␈α However,␈αthe␈αprogrammer␈αcannot␈αtell␈αthe
␈↓ α∧␈↓computer␈α
to␈αdo␈α
this␈α
without␈αreading␈α
much␈αof␈α
the␈α
existing␈αprogram.␈α
 As␈α
much␈αas␈α
possible,␈αwe␈α
need
␈↓ α∧␈↓to be able to change programs without reading them.

␈↓ α∧␈↓␈↓ αTb.␈α
In␈α
natural␈α
language,␈α
we␈α
don't␈α
usually␈αhave␈α
to␈α
specify␈α
data␈α
structures.␈α
 For␈α
example,␈αthe
␈↓ α∧␈↓airline␈α∞official␈α∞originally␈α∞specifying␈α∞a␈α∞reservation␈α∞system␈α∞might␈α∞say:␈α∞The␈α∞program␈α∞should␈α∞accept
␈↓ α∧␈↓reservations␈α
if␈α
the␈α
number␈α
of␈α
reservations␈α
is␈α
less␈α
than␈α
the␈α
capacity␈α
of␈α
the␈α
flight,␈α
it␈α
should␈α
allow
␈↓ α∧␈↓the␈α
passenger␈αto␈α
cancel␈α
a␈αreservation,␈α
and␈αit␈α
should␈α
answer␈αwhen␈α
asked␈α
whether␈αa␈α
passenger␈αhas␈α
a
␈↓ α∧␈↓reservation.␈α∪ There␈α∪is␈α∪nothing␈α∪in␈α∪this␈α∪specification␈α∪about␈α∪a␈α∪data␈α∪structure␈α∪for␈α∩remembering
␈↓ α∧␈↓reservations,␈αand␈αwe␈αcan␈αimagine␈α
a␈αcompiler␈αfor␈αa␈αlanguage␈α
that␈αwould␈αdecide␈αon␈αa␈αdata␈α
structure
␈↓ α∧␈↓only␈αafter␈αthe␈αdesired-input␈αoutput␈αbehavior␈αis␈αspecified.␈α The␈αkey␈αfact␈αis␈αthat␈αa␈αpassenger␈αhas␈αa
␈↓ α∧␈↓reservation␈αif␈αhe␈αhas␈αmade␈αone␈αand␈αnot␈αcancelled␈αit.␈α A␈αprogramming␈αlanguage␈αthat␈αallowed␈αthis
␈↓ α∧␈↓to␈α∂be␈α∂said␈α∞has␈α∂to␈α∂allow␈α∞statements␈α∂to␈α∂refer␈α∞to␈α∂the␈α∂occurrence␈α∞of␈α∂past␈α∂events␈α∞rather␈α∂than␈α∂to␈α∞the
␈↓ α∧␈↓present␈α∂status␈α∞of␈α∂a␈α∞data␈α∂structure␈α∂into␈α∞which␈α∂information␈α∞has␈α∂been␈α∞stored.␈α∂ The␈α∂compiler␈α∞itself
␈↓ α∧␈↓should decide to use an array of length equal to the number of seats on the flight.

␈↓ α∧␈↓␈↓ αTTo␈α
see␈αthat␈α
this␈α
represents␈αa␈α
decision␈αby␈α
the␈α
compiler,␈αimagine␈α
that␈αthe␈α
official␈α
decided␈αto
␈↓ α∧␈↓modify␈α∩the␈α∩procedure␈α⊃so␈α∩that␈α∩it␈α∩could␈α⊃be␈α∩answered␈α∩whether␈α∩as␈α⊃passenger␈α∩had␈α∩ever␈α∩made␈α⊃a
␈↓ α∧␈↓reservation.␈α∂ Then␈α⊂the␈α∂compiler␈α⊂would␈α∂require␈α⊂a␈α∂different␈α∂data␈α⊂structure,␈α∂since␈α⊂it␈α∂is␈α⊂no␈α∂longer
␈↓ α∧␈↓permissible to forget cancelled reservations.

␈↓ α∧␈↓␈↓ αTIt␈α⊃is␈α⊃even␈α⊂more␈α⊃powerful␈α⊃to␈α⊃allow␈α⊂reference␈α⊃to␈α⊃the␈α⊂future.␈α⊃ "Baggage␈α⊃handlers␈α⊃shall␈α⊂be
␈↓ α∧␈↓summoned␈αto␈αthe␈αairport␈αone␈αhour␈αbefore␈αthe␈αairplane␈αarrives".␈α A␈αlanguage␈αpermitting␈αreference
␈↓ α∧␈↓to␈α∂the␈α∂future␈α∂may␈α∂contain␈α∂contradictory␈α∂programs␈α∂which␈α∂therefore␈α∂couldn't␈α∂be␈α⊂compiled.␈α∂ Most
␈↓ α∧␈↓likely␈α⊂it␈α∂will␈α⊂be␈α⊂undecidable␈α∂in␈α⊂general␈α∂whether␈α⊂a␈α⊂futuristic␈α∂program␈α⊂is␈α⊂compilable.␈α∂ However,
␈↓ α∧␈↓compilers will be able to try and know whether or not they have succeeded.

␈↓ α∧␈↓␈↓ αTI␈α∂have␈α∞been␈α∂trying␈α∂to␈α∞specify␈α∂a␈α∞programming␈α∂language␈α∂called␈α∞Elephant␈α∂(it␈α∂never␈α∞forgets)
␈↓ α∧␈↓that would allow such programs.
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓␈↓ αTc.␈α∀Present␈α∀programming␈α∀languages␈α∪for␈α∀describing␈α∀concurrent␈α∀processes␈α∀require␈α∪explicit
␈↓ α∧␈↓attention␈α∂to␈α∞synchronization,␈α∂fairness,␈α∂etc.␈α∞ Natural␈α∂language␈α∞description␈α∂of␈α∂concurrent␈α∞processes
␈↓ α∧␈↓rarely has to be explicit about such matters.

␈↓ α∧␈↓␈↓ αTd.␈αThe␈αmeta-problem␈αis␈αto␈α
identify␈αother␈αsemantic␈αfeatures␈αof␈αnatural␈α
language␈αdescription
␈↓ α∧␈↓of procedures that aren't in present programming languages.

␈↓ α∧␈↓␈↓ αT3.␈α⊃Common␈α⊃business␈α⊃communication␈α⊃language.␈α∩ This␈α⊃is␈α⊃a␈α⊃problem␈α⊃on␈α⊃the␈α∩boundary␈α⊃of
␈↓ α∧␈↓computer␈α
science,␈α
artificial␈α
intelligence,␈α
linguistics␈α
and␈α
business.␈α
 The␈α
full␈α
utility␈α
of␈α∞computers␈α
in
␈↓ α∧␈↓business␈α∪requires␈α∩that␈α∪computers␈α∪belonging␈α∩to␈α∪different␈α∩organizations␈α∪communicate␈α∪with␈α∩one
␈↓ α∧␈↓another␈α∪-␈α∩even␈α∪computers␈α∩whose␈α∪owners␈α∪have␈α∩never␈α∪heard␈α∩of␈α∪each␈α∩other.␈α∪ For␈α∪example,␈α∩a
␈↓ α∧␈↓Company␈αA's␈α
computer␈αmight␈αextract␈α
the␈αfact␈αthat␈α
company␈αB's␈αcomputer␈α
supplies␈αwidgets␈αfrom␈α
a
␈↓ α∧␈↓database,␈αthen␈αtelephone␈αCompany␈αB's␈αcomputer␈αand␈αask␈αwhat␈αprice␈αand␈αdelivery␈αis␈αavailable␈αon
␈↓ α∧␈↓300␈αNumber␈α5␈αwidgets,␈αeach␈αwith␈α8␈αmegabytes␈αof␈αmemory␈αand␈αwhite␈αsidewall␈αtires.␈α Company␈αB's
␈↓ α∧␈↓computer␈αmight␈αrespond␈αwith␈αa␈αprice␈αand␈αa␈αstatement␈αthat␈αthey␈αcould␈αbe␈αdelivered␈αstarting␈αin␈αsix
␈↓ α∧␈↓months␈α⊂at␈α⊂a␈α⊂rate␈α⊃of␈α⊂20␈α⊂per␈α⊂month␈α⊂provided␈α⊃the␈α⊂production␈α⊂capacity␈α⊂wasn't␈α⊂pre-empted␈α⊃by␈α⊂a
␈↓ α∧␈↓Government order.

␈↓ α∧␈↓␈↓ αTThis␈α⊃relatively␈α⊃fancy␈α⊃example␈α∩illustrates␈α⊃the␈α⊃fact␈α⊃that␈α⊃standardizing␈α∩such␈α⊃intercomputer
␈↓ α∧␈↓business␈α∀communication␈α∀requires␈α∀formalization␈α∀of␈α∀an␈α∀interesting␈α∀subset␈α∀of␈α∀natural␈α∪language
␈↓ α∧␈↓semantics.  See (McCarthy 1982) for more of this.

␈↓ α∧␈↓References:

␈↓ α∧␈↓␈↓αMcCarthy,␈α∞John␈α∞(1965)␈↓:␈α∞"Problems␈α∞in␈α∞the␈α∞Theory␈α∞of␈α∞Computation",␈α∞in␈α∞Proc.␈α∞ IFIP␈α∞Congress␈α
65,
␈↓ α∧␈↓Spartan, Washington, D.C..

␈↓ α∧␈↓␈↓αCartwright,␈αR.S.␈α(1977)␈↓:␈α
␈↓↓A␈αPractical␈αFormal␈α
Semantic␈αDefinition␈αand␈α
Verification␈αSystem␈αfor␈α
Typed
␈↓ α∧␈↓↓Lisp␈↓, Ph.D. Thesis, Computer Science Department, Stanford University, Stanford, California.

␈↓ α∧␈↓␈↓αCartwright,␈α⊃Robert␈α⊂and␈α⊃John␈α⊂McCarthy␈α⊃(1979)␈↓:␈α⊃"Recursive␈α⊂Programs␈α⊃as␈α⊂Functions␈α⊃in␈α⊃a␈α⊂First
␈↓ α∧␈↓Order␈α∀Theory",␈α∃in␈α∀␈↓↓Proceedings␈α∃of␈α∀the␈α∃International␈α∀Conference␈α∃on␈α∀Mathematical␈α∃Studies␈α∀of
␈↓ α∧␈↓↓Information Processing␈↓, Kyoto, Japan.

␈↓ α∧␈↓␈↓αMcCarthy,␈α
John␈α
(1982)␈↓:␈α
"Common␈α
Business␈α
Communication␈α
Language",␈α
in␈α∞␈↓↓Textverarbeitung␈α
und
␈↓ α∧␈↓↓B␈↓
:␈↓↓urosysteme␈↓,␈α
Albert␈αEndres␈α
and␈αJ␈↓
:␈↓urgen␈α
Reetz,␈αeds.␈α
 R.␈αOldenbourg␈α
Verlag,␈αMunich␈α
and␈αVienna
␈↓ α∧␈↓1982.